The present invention pertains to a method for ordering reduced ordered binary decision diagrams (ROBDDS) in the formal equivalence verification of digital designs. More particularly, the present invention pertains to producing an efficient ordering for ROBDDs to reduce the run time of equivalence verification in digital designs.
As is known in the art, a Boolean function is a mapping that gives a Boolean value for a given combination of input values. Many problems in the computer-aided design (CAD) for digital circuits can be represented as a set of operations performed over a set of Boolean functions. Hence, efficient representation and manipulation of Boolean functions is an important component of digital designs. For example, when comparing and verifying equivalence between the register transfer language (RTL) and the detailed logic drawing of a schematic, both models can be compiled into an intermediate form representing Boolean equations for the outputs of both the models. The Boolean equations are then compared for each output during equivalence verification of the models.
Various representations of Boolean functions are possible, including Boolean equations, truth tables, and binary decision diagrams (BDDs). A BDD is a directed acyclic graph (DAG). The branching graph represents a combination of input values leading to an output value, with each node representing an input variable and each edge representing the value of the given variable. Each path from the source input to each sink output represents an assignment of values of all inputs. An ordered binary decision diagram (OBDD) is a BDD with the constraint that the input variables are ordered and every source to sink path in the OBDD visits the input variable in the same order.
Nodes in an OBBD can be eliminated via node sharing and by removing redundant nodes. The resulting graph is called a reduced order binary decision diagram (ROBDD). A ROBDD is an OBDD where each node represents a distinct logic function.
Furthermore, for a given Boolean function and for a fixed ordering, there exists a single unique ROBDD. While many different Boolean equations may represent a single Boolean function, the fixed ordered ROBDD for a given Boolean function is unique. Hence, equivalence of corresponding ROBDDs (i.e. ROBDDs that match node for node) implies functional equivalence. As such, ROBDDs are utilized in formal equivalence verification for possessing inherent properties for representing Boolean functions both compactly and uniquely.
Ordering of the input variables is crucial in determining the size of the ROBDD (i.e. the number of nodes). Depending on the order of inputs for an equation with N inputs, the number of nodes can be exponential in N or very small. Thus, an efficient ordering can lead to significant reduction of nodes, and thereby, a reduced run-time in equivalence verification.
As is known in the art, formal equivalence verification involves proving the equivalence of two designs. To prove that both designs are equivalent, each processor design to be simulated is compiled into an intermediate format which can be used to build ROBDDs for comparison. Current tools which produce the ordering of input variables do so based on generic Boolean equations without utilizing some of the characteristics present in Boolean equations which describe digital designs. Formal equivalence verification tools using these methods may not run within a reasonable amount of time or fail to complete due to inefficient or incomplete ordering of variables.
In view of the above, there is a need for an improved method for ordering ROBDDs used in the equivalence verification of processors.